Nuprl Lemma : comb_for_l_member_wf
4,23
postcript
pdf
(
T
,
x
,
l
,
z
. (
x
l
))
T
:Type
T
(
T
List)
True
Prop
latex
Definitions
True
,
t
T
,
x
:
A
.
B
(
x
)
,
T
Lemmas
l
member
wf
,
squash
wf
,
true
wf
origin
T,x,l,z. (x 
l)) T:Type
T(T List)
TrueProp T,x,l,z. (x l)) T:TypeT(T List)TrueProp T
x:A. B(x)T